/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979

␈↓ ↓H␈↓α␈↓ ¬FTERM PROJECTS

␈↓ ↓H␈↓        A␈αterm␈αproject␈αis␈αnot␈αrequired␈αin␈αorder␈αto␈αpass␈αCS206␈αor␈αeven␈αto␈αget␈αa␈αgrade␈αof␈αB␈αif␈αyour
␈↓ ↓H␈↓homework␈α
and␈α
exams␈αare␈α
good␈α
enough.␈α However,␈α
if␈α
you␈α
wish␈αto␈α
get␈α
some␈αflavor␈α
of␈α
A␈αthen␈α
doing
␈↓ ↓H␈↓a␈αgood␈α
term␈αproject␈αis␈α
necessary.␈α Term␈α
projects␈αwill␈αbe␈α
due␈αon␈α
the␈αday␈αof␈α
the␈αfinal␈α
exam.␈α Any
␈↓ ↓H␈↓term project turned in ahead of time will be likely to get a more thorough reading.

␈↓ ↓H␈↓        The␈αterm␈αproject␈αis␈αyour␈αopportunity␈αto␈αdirect␈αyour␈αattention␈αto␈αand␈αget␈αexperience␈αin␈αsome
␈↓ ↓H␈↓area␈αthat␈αinterests␈αyou.␈α  It␈αmay␈αbe␈αprogramming␈αor␈αtheoretical␈αor␈αboth.␈α  A␈αprogramming␈αproject
␈↓ ↓H␈↓may␈α⊂be␈α⊂related␈α⊂to␈α⊂computing␈α⊂(a␈α⊂compiler),␈α⊂AI␈α⊂(game␈α⊂playing,␈α⊂problem␈α⊂solving)␈α⊂other␈α⊂areas␈α⊂of
␈↓ ↓H␈↓computer␈αscience,␈αor␈αsome␈αunrelated␈αarea␈αin␈αwhich␈αyou␈αhave␈αinterest␈αand␈αexpertise.␈α A␈αtheoretical
␈↓ ↓H␈↓project␈αshould␈αrelate␈αto␈αreasoning␈αabout␈αLISP␈αprograms.␈α  Some␈αideas␈αare␈αgiven␈αbelow.␈α Feel␈αfree
␈↓ ↓H␈↓to design your own project.

␈↓ ↓H␈↓        The␈α
write␈α
up␈α
of␈α
your␈α
project␈α
is␈α
the␈α
main␈α
thing␈α
that␈α
will␈α
get␈α
graded␈α
so␈α
it␈α
should␈α
be␈α
clear␈α
and
␈↓ ↓H␈↓carefully␈α∂done.␈α∂ It␈α∂should␈α∂include␈α∞a␈α∂brief␈α∂description␈α∂of␈α∂what␈α∂you␈α∞set␈α∂out␈α∂to␈α∂do␈α∂and␈α∂what␈α∞you
␈↓ ↓H␈↓accomplished.␈α∞ If␈α∞you␈α
write␈α∞a␈α∞progam,␈α
you␈α∞should␈α∞give␈α
a␈α∞description␈α∞of␈α
how␈α∞it␈α∞works␈α∞and␈α
why,
␈↓ ↓H␈↓including␈α∞a␈α∞description␈α∂of␈α∞the␈α∞data␈α∂structures␈α∞it␈α∞is␈α∂acting␈α∞on␈α∞and␈α∂the␈α∞basic␈α∞operations␈α∂on␈α∞these
␈↓ ↓H␈↓structures.␈α∂ The␈α∂code␈α∂for␈α∂the␈α∂program␈α∂should␈α∂be␈α∂included␈α∂with␈α∂brief␈α∂comments␈α∂in␈α∂appropriate
␈↓ ↓H␈↓places to guide the reader.  Some sample runs should also be included.

␈↓ ↓H␈↓        Before␈α
putting␈α
a␈α
lot␈α
of␈α
work␈α
into␈α
your␈α
project,␈α
you␈α
should␈α
outline␈α
carefully␈α
just␈α
what␈αyou
␈↓ ↓H␈↓plan␈α∞to␈α∞do␈α∞and␈α∞have␈α∞this␈α∞approved␈α∞by␈α∞the␈α∞instructor␈α∞or␈α∞the␈α∞TA.␈α∞  You␈α∞are␈α∞also␈α∞encouraged␈α∞to
␈↓ ↓H␈↓discuss initial ideas before finalizing your plans.


␈↓ ↓H␈↓αProving

␈↓ ↓H␈↓1.␈α
Develop␈α
and␈αapply␈α
techniques␈α
for␈αproving␈α
properties␈α
of␈αprograms␈α
manipulating␈α
graphs.␈α The
␈↓ ↓H␈↓proofs␈αshould␈αbe␈αfully␈αformal,␈αbut␈αalso␈αnatual␈αand␈αcleanly␈αexpressible.␈α Some␈αparticular␈αproblems
␈↓ ↓H␈↓to␈α
be␈α
considered␈α
are␈αformalizing␈α
abstractly␈α
the␈α
notions␈αof␈α
graph,␈α
path,␈α
component,␈α
etc.␈α Showing
␈↓ ↓H␈↓that␈αa␈αparticular␈αS-expression␈αrepresentation␈αof␈αgraphs␈αsatisfy␈αthe␈αsame␈αproperties␈αas␈αthe␈αabstract
␈↓ ↓H␈↓notion.␈α∞ Developing␈α∂principles␈α∞for␈α∞proving␈α∂that␈α∞programs␈α∞on␈α∂graphs␈α∞terminate.␈α∂ Specifying␈α∞and
␈↓ ↓H␈↓proving␈α
correctness␈αof␈α
some␈α
graph␈αprograms␈α
(list␈α
all␈αnodes,␈α
find␈α
a␈αpath␈α
from␈α
␈↓↓v1␈↓␈αto␈α
␈↓↓v2,␈↓␈α
find␈αthe
␈↓ ↓H␈↓shortest␈αpath,␈αetc.␈α     [Remark:␈α for␈α
a␈αterm␈αproject␈αyou␈αexpected␈αonly␈α
to␈αsolve␈αa␈αselect␈αfew␈αof␈α
these
␈↓ ↓H␈↓problems, not all of them.]

␈↓ ↓H␈↓2.␈α Develop␈αthe␈αtheory␈αof␈αre-entrant␈α
list␈αstructures.␈α (see␈αChapter␈αIV.)␈αDecide␈αon␈α
a␈αrepresentation
␈↓ ↓H␈↓of␈α∀such␈α∃structures␈α∀as␈α∀ordinary␈α∃lists␈α∀(say␈α∃with␈α∀pointers␈α∀and␈α∃labels).␈α∀ Define␈α∃some␈α∀primitive
␈↓ ↓H␈↓operations␈α(for␈αexample:␈α␈↓↓car␈αcdr␈αcons␈αpoint␈αcut␈↓).␈α Write␈αprograms␈αto␈αgo␈αfrom␈αone␈αrepresentation␈αto
␈↓ ↓H␈↓the␈α∂other.␈α∂ Write␈α∞an␈α∂equality␈α∂predicate␈α∂in␈α∞for␈α∂structures␈α∂in␈α∞your␈α∂representation.␈α∂  Work␈α∂out␈α∞an
␈↓ ↓H␈↓induction␈α∂schema␈α∂to␈α∞allow␈α∂you␈α∂to␈α∂tell␈α∞when␈α∂programs␈α∂on␈α∞such␈α∂structures␈α∂will␈α∂terminate.␈α∞ Write
␈↓ ↓H␈↓some interesting programs on such structures and prove some facts about them.

␈↓ ↓H␈↓3.␈α∂ Prove␈α∂a␈α∂moderate␈α∂size␈α∂"practical"␈α∂program␈α∂correct.␈α∂ For␈α∂example␈α∂a␈α∂modest␈α∂pattern␈α∞matcher,
␈↓ ↓H␈↓unifier, or  simple production rule system would be appropriate.
␈↓ ↓H␈↓2␈↓ H


␈↓ ↓H␈↓αFormal systems

␈↓ ↓H␈↓4.␈αWrite␈α
a␈αproof␈α
checker␈αfor␈αa␈α
simple␈αformal␈α
system.␈α  Some␈αexamples␈α
of␈αsuitable␈α
formal␈αsystems
␈↓ ↓H␈↓are:

␈↓ ↓H␈↓␈↓ αH4.1. Trigonometric expressions: using trig identities to prove expressions equivalent.
␈↓ ↓H␈↓␈↓ αH4.2.␈αSymbolic␈α
integration:␈αusing␈αvarious␈α
standard␈αtricks␈α
for␈αmanipulating␈αintegrands␈α
into
␈↓ ↓H␈↓␈↓ αHintegrable form.
␈↓ ↓H␈↓␈↓ αH4.3. Propositional logic and a Hilbert or natural deduction style proof system.

␈↓ ↓H␈↓␈↓ αHSome "bells and whistles" that you might consider adding to your system include:

␈↓ ↓H␈↓␈↓ αH4.4. Implement some heuristics to search for proofs.
␈↓ ↓H␈↓␈↓ αH4.5.␈α⊂Implement␈α⊂some␈α⊂derived␈α⊂rules␈α⊂plus␈α⊂the␈α⊂ability␈α⊂to␈α⊂expand␈α⊂a␈α⊂deduction␈α⊂using␈α⊂the
␈↓ ↓H␈↓␈↓ αHderived rule into one consisting only of elementary steps.


␈↓ ↓H␈↓αCompiling

␈↓ ↓H␈↓5. Improve the LCOM4 compiler.  Some possibilities are to modify LCOM4 to:

␈↓ ↓H␈↓␈↓ αH5.1. compile  ␈↓↓label.␈↓
␈↓ ↓H␈↓␈↓ αH5.2. handle the ␈↓αprog␈↓ and related features.
␈↓ ↓H␈↓␈↓ αH5.3. handle functions as arguments (as for ␈↓↓mapcar)␈↓ .
␈↓ ↓H␈↓␈↓ αH5.4. recognize iteration and compile it with loops.
␈↓ ↓H␈↓␈↓ αH5.5. produce more efficient arithmetic code.
␈↓ ↓H␈↓␈↓ αH5.6. compile additional features such as "while's" or "do's" etc..

␈↓ ↓H␈↓6. Write a data driven compiler for LISP.

␈↓ ↓H␈↓7.␈α⊂Write␈α⊂a␈α⊂syntax␈α⊂directed␈α⊂compiler␈α⊂for␈α⊂LISP.␈α⊂  Perhaps␈α⊂several␈α⊂passes␈α⊂using␈α⊃an␈α⊂intermediate
␈↓ ↓H␈↓␈↓ αλlanguage would be useful.


␈↓ ↓H␈↓αGames

␈↓ ↓H␈↓8. Write a program to play a game.  Some possible games are:

␈↓ ↓H␈↓␈↓ αH8.1. 3-dimensional Tic Tac Toe (See forthcoming Chapter for 2-D version.)
␈↓ ↓H␈↓␈↓ αH8.2. Solitare
␈↓ ↓H␈↓␈↓ αH8.3. Mastermind
␈↓ ↓H␈↓␈↓ αH8.4. Otello

␈↓ ↓H␈↓    There␈α∞are␈α
two␈α∞key␈α∞issues␈α
in␈α∞programs␈α∞to␈α
play␈α∞games.␈α∞ One␈α
is␈α∞the␈α∞method␈α
used␈α∞to␈α∞prune␈α
the
␈↓ ↓H␈↓␈↓ αλsearch␈αfor␈αpossible␈αmoves,␈αthe␈αother␈αis␈αdeveloping␈αgood␈αstrategies␈αof␈αchoosing␈αmoves.␈α These
␈↓ ↓H␈↓␈↓ αλissues are of course not independent from one another.

␈↓ ↓H␈↓    Be␈α⊂sure␈α⊂to␈α⊂hold␈α⊂individual␈α⊂test␈α∂runs␈α⊂to␈α⊂a␈α⊂few␈α⊂seconds.␈α⊂ It␈α∂is␈α⊂easy␈α⊂to␈α⊂use␈α⊂large␈α⊂amounts␈α∂of
␈↓ ↓H␈↓␈↓ αλcomputer time in such projects.
␈↓ ↓H␈↓␈↓ 93


␈↓ ↓H␈↓αAIish programs

␈↓ ↓H␈↓9.␈α∞ Write␈α∞a␈α∞program␈α∞that␈α∞generates␈α∞form␈α∞letters.␈α
 You␈α∞should␈α∞have␈α∞a␈α∞particular␈α∞class␈α∞of␈α∞user␈α
in
␈↓ ↓H␈↓␈↓ αλmind,␈αsay␈α
a␈αbusiness,␈αor␈α
political␈αgroup.␈α
 It␈αshould␈αdeal␈α
with␈αa␈αvariety␈α
of␈αsituations␈α
and␈αthe
␈↓ ↓H␈↓␈↓ αλresulting letter should depend in an interesting way on set of facts about recipient of letter.

␈↓ ↓H␈↓10.␈αA␈αnatural␈αlanguage␈αprogram,␈αfor␈αexample␈α
a␈αprogram␈αthat␈αdoes␈αmorphemic␈αanalysis␈αof␈α
english.
␈↓ ↓H␈↓␈↓ αλYou should have a clearly defined class of words that can be analyzed by your program.


␈↓ ↓H␈↓αData manipulating programs.

␈↓ ↓H␈↓11.  Write a program that does file cross referencing for some interesting class of files.

␈↓ ↓H␈↓12.␈α Answering␈αquestions␈αabout␈αa␈α
data␈αbase␈αof␈αfacts.␈α Assume␈α
you␈αhave␈αa␈αfinite␈αdomain␈αof␈α
objects
␈↓ ↓H␈↓␈↓ αλand␈α⊂a␈α∂data␈α⊂base␈α⊂of␈α∂facts␈α⊂about␈α⊂these␈α∂objects.␈α⊂ For␈α∂example␈α⊂assume␈α⊂that␈α∂there␈α⊂is␈α⊂a␈α∂given
␈↓ ↓H␈↓␈↓ αλcollection␈αof␈αrelations␈αthat␈αapply␈αto␈αthe␈αobjects␈αand␈αall␈αtrue␈αinstances␈αof␈αthese␈αrelations␈αare␈αin
␈↓ ↓H␈↓␈↓ αλthe␈α
data␈α
base.␈α
 (The␈α
closed␈α
world␈α
assumption.)␈α
  Write␈α
a␈α
program␈α
that␈α
decides␈α
the␈α
truth␈α
or
␈↓ ↓H␈↓␈↓ αλfalsity␈αof␈α
any␈αfirst␈α
order␈αsentence␈αbuilt␈α
from␈α the␈α
given␈αrelation␈α
symbols,␈αvariables␈αand␈α
names
␈↓ ↓H␈↓␈↓ αλof␈α⊂the␈α⊃objects.␈α⊂ An␈α⊂interesting␈α⊃and␈α⊂useful␈α⊂extension␈α⊃is␈α⊂to␈α⊂allow␈α⊃a␈α⊂formula␈α⊂with␈α⊃one␈α⊂free
␈↓ ↓H␈↓␈↓ αλvariable and have the program return one or more objects (if any) that satisfy the formula.


␈↓ ↓H␈↓αSome previous projects.

␈↓ ↓H␈↓13. Minimizing finite state machines

␈↓ ↓H␈↓14.␈αDigital␈α
Circuit␈αdesign:␈α
 design␈αrepresentation␈αof␈α
gates␈αand␈α
circuits.␈α Implement␈α
algorithms␈αfor
␈↓ ↓H␈↓␈↓ αλoptimizing circuit designs or layouts.

␈↓ ↓H␈↓15. LALR parser